Inference at * 1 1 1 2 1 
Iof proof for Lemma decidable implies better:



1. P : 
2. Q : x:P.
3. P
4. Q
5. Q  
  (P  Q)  ((P  Q)) 

latex

 by OrLeft THEN Auto 

latex

 .

Definitions	P  Q, A, x:A. B(x), P  Q, , t  T
Lemmas	not wf